This invention relates to hardware and software design verification.
One facet of hardware/software co-design is dealing with verification at the hardware/software interface. In the typical case where the hardware and software are designed separately, a common problem is that the expectations of each design group do not match the implementation of the other. This is particularly true in situations where the hardware and the software interact extensively, with each part controlling the behavior of the other. When such interfaces are not properly handled, logical failures are likely to result, with attendant costly delays in production. The familiar presumption that the hardware and the software each can be designed successfully with only a sketchy understanding of the other side is unwarranted in complex systems. Each design team needs a precise description of its "environment" as defined by the other design. If formal models of the hardware design and the software design are used in support of this need, the problem of interface mismatch is moved to a problem of how to develop a design in the context of a formal environment description.
Conceptually, formal verification could offer a solution to this problem. However, direct application of model-checking in this context is mostly infeasible, because each side individually is often near the limit of feasible verification. Moreover, there is an intrinsic difficulty in applying finite-state verification to software, which often is viewed as an infinite-state system on account of its dependence on memory.
While hardware/software co-design has been treated extensively in terms of methodology, no viable methods have been published on formal co-verification. The co-verification problem is treated mainly as a testing problem, and a number of commercial tools have appeared for testing software in the context of hardware, and vice versa.
Apart from the above, partial order reduction and symbolic state space search have been applied widely to cope with the intrinsic computational complexity of modelchecking. Typically, these techniques are applied separately--only one or the other--since they appear to be incompatible. Partial order reduction algorithms found in the literature are based intrinsically on explicit state enumeration in the context of a depth-first search. The partial order reduction found in the prior art is derived dynamically in the course of enumerating the states. Symbolic verification deals only with sets of states defined by respective Boolean functions. State reachability is expressed in terms of the convergence of a monotone state set operator which implements a breadth-first search of the state space.
What makes partial order reduction problematic in this context has to do with guaranteeing that certain transitions which may be deferred in the course of the state space search (thus giving rise to the desired reduction), are not deferred indefinitely (resulting in an incomplete search). The usual way this is implemented in the context of explicit-state enumeration, is to explore all such deferred transitions in the course of closing any cycle during a depth-fist search.
Nonetheless, there is no intrinsic reason that partial order reduction and symbolic verification cannot be combined. Perhaps the first published proposal for such a combination is presented by R. Alur, R. K. Brayton, T. A. Henzinger, S. Qadeer, and S. K. Rajarnani, in "Partial order reduction in symbolic state space exploration," Conference on Computer Aided Verification (CAV 97), LNCS 1254, Springer-Verlag, (1997) pp 340-351. In that paper, the cycle-closing condition is replaced by some additional steps in the course of the symbolic breadth-first search, and those additional steps require the normal modelchecking algorithm to be altered.